theory Clang imports Main
begin

datatype val_tp               --"data types of variables"
   = BoolT | NatT             --"boolean, natural numbers"

datatype vals                 --"program values"
   = BoolV bool | NatV nat    --"boolean, natural numbers" 

datatype 'n expr =            --"expression; 'n - variable names"
    Evar 'n                   --"variable"
  | Eimm vals                 --"immediate value"

datatype 'n bexpr =           --"boolean expression"
    Bex "'n expr"             --"boolean-valued expression"
  | Beq "'n expr" "'n expr"   --"equal"
  | Bneq "'n expr" "'n expr"  --"not equal"

datatype ('n,'m) wcond =      --"wait condition; 'n-local vars, 'm-shared vars"
    Weq 'm "'n expr"          --"shared var = expr on local vars/constants"
  | Wneq 'm "'n expr"         --"not equal"

--"disjunction of wait conditions"
type_synonym ('n,'m) wconds = "('n,'m) wcond list"

--"program statement; 'n-local variables, 'm-shared variables"
datatype ('pn,'n,'m,'l) stmt =
--"no operation"
   Cnone "'l option"
--"sequential execution"
 | Cseq  "'l option" "('pn,'n,'m,'l) stmt" "('pn,'n,'m,'l) stmt"
--"v1:=v2 where v1, v2 are local variables"
 | Casg  "'l option" 'n "'n expr"
--"if (expr on locals) then stmt1 else stmt2"
 | Cif   "'l option" "'n bexpr" "('pn,'n,'m,'l) stmt" "('pn,'n,'m,'l) stmt"
--"while (expr on locals) do stmt"
 | Cwhile "'l option" "'n bexpr" "('pn,'n,'m,'l) stmt"
--"read x s: read shared s into local x"
 | Cread "'l option" 'n 'm
--"write the value of a local expression to shared variables"
 | Cwrite "'l option" 'm "'n expr"
--"wait for one of the conditions"
 | Cwait  "'l option" "('n,'m) wconds" "('pn,'n,'m,'l) stmt"

fun stmlab :: "('pn,'n,'m,'l) stmt ~=> 'l"
where
  "stmlab (Cnone lb)     = lb"
| "stmlab (Cseq lb _ _)  = lb"
| "stmlab (Casg lb _ _)  = lb"
| "stmlab (Cif lb _ _ _) = lb"
| "stmlab (Cwhile lb _ _) = lb"
| "stmlab (Cread lb _ _)  = lb"
| "stmlab (Cwrite lb _ _) = lb"
| "stmlab (Cwait lb _ _)  = lb"

fun wcs_of_wait where "wcs_of_wait (Cwait _ wcs _) = Some wcs" | "wcs_of_wait _ = None"

datatype 'n vdecl           --"variable declaration (name, data type)"
    = Vdecl 'n val_tp

fun vd_name :: "'n vdecl \<Rightarrow> 'n"     where "vd_name (Vdecl x _) = x"
fun vd_type :: "'n vdecl \<Rightarrow> val_tp" where "vd_type (Vdecl _ tp) = tp"

type_synonym 'n vctx = "'n vdecl list"     --"var declaration list"

datatype ('pn,'n,'m) phdr   --"process header (process name, locals, shared)"
    = Phdr "'pn" "('n vdecl list)" "('m vdecl list)"

fun hdr_ctx   :: "('pn,'n,'m) phdr \<Rightarrow> 'n vctx" 
  where "hdr_ctx   (Phdr _ vds _) = vds"
fun hdr_ctxsh :: "('pn,'n,'m) phdr \<Rightarrow> 'm vctx" 
  where "hdr_ctxsh (Phdr _ _ vds) = vds"

datatype ('pn,'n,'m,'l) proc   --"process (header, code)"
    = Proc "('pn,'n,'m) phdr" "('pn,'n,'m,'l) stmt"

fun proc_name  :: "('pn,'n,'m,'l) proc \<Rightarrow> 'pn"
  where "proc_name (Proc (Phdr nm _ _) _) = nm"
fun proc_ctx   :: "('pn,'n,'m,'l) proc \<Rightarrow> 'n vctx" 
  where "proc_ctx (Proc hdr _) = (hdr_ctx hdr)"
fun proc_ctxsh :: "('pn,'n,'m,'l) proc \<Rightarrow> 'm vctx" 
  where "proc_ctxsh (Proc hdr _) = (hdr_ctxsh hdr)"
fun proc_stm :: "('pn,'n,'m,'l) proc \<Rightarrow> ('pn,'n,'m,'l) stmt" 
  where "proc_stm (Proc _ stm) = stm"

--"combined program (list of processes)"
type_synonym ('pn,'n,'m,'l) prog = "('pn,'n,'m,'l) proc list"

primrec vals_tp :: "vals \<Rightarrow> val_tp"             --"get type of value"
where
  "vals_tp (BoolV b) = BoolT"
 |"vals_tp (NatV n) = NatT"

definition var_tp :: "'n vctx \<Rightarrow> 'n ~=> val_tp" --"get type of var"
where
  "var_tp ctx v = foldl (\<lambda> res vd . 
                            if (res = None \<and> (vd_name vd = v)) 
                             then Some (vd_type vd) 
                             else res
                        ) None ctx"

fun expr_tp :: "'n vctx \<Rightarrow> 'n expr ~=> val_tp"  --"get type of expr"
where
  "expr_tp ctx (Evar v) = (var_tp ctx v)"
 |"expr_tp ctx (Eimm i) = Some (vals_tp i)"

fun wt_var :: "'n vctx \<Rightarrow> 'n \<Rightarrow> bool"            --"check if var is defined"
where
  "wt_var ctx e = (case (var_tp ctx e) of 
                          (Some _) \<Rightarrow> True 
                        | None \<Rightarrow> False)"

fun wt_expr :: "'n vctx \<Rightarrow> 'n expr \<Rightarrow> bool"      --"check if expr is defined"
where
  "wt_expr ctx e = (case (expr_tp ctx e) of 
                          (Some _) \<Rightarrow> True 
                        | None \<Rightarrow> False)"

fun wt_bexpr :: "'n vctx \<Rightarrow> 'n bexpr \<Rightarrow> bool" --"check if boolean expr is defined"
where
  "wt_bexpr ctx (Bex e) = (case (expr_tp ctx e) of 
                                    (Some BoolT) \<Rightarrow> True
                                    | _ \<Rightarrow> False )"

 |"wt_bexpr ctx (Beq e1 e2) = ( wt_expr ctx e1 
                              \<and> expr_tp ctx e1 = expr_tp ctx e2 )"

 |"wt_bexpr ctx (Bneq e1 e2) = ( wt_expr ctx e1 
                               \<and> expr_tp ctx e1 = expr_tp ctx e2 )"

fun wt_waitcond :: "'n vctx \<Rightarrow> 'm vctx \<Rightarrow> ('n,'m) wcond \<Rightarrow> bool"
where
  "wt_waitcond loc sh (Weq x e) = ( wt_var sh x 
                                  \<and> wt_expr loc e 
                                  \<and> var_tp sh x = expr_tp loc e )"

| "wt_waitcond loc sh (Wneq x e) = ( wt_var sh x 
                                   \<and> wt_expr loc e 
                                   \<and> var_tp sh x = expr_tp loc e )"

fun wt_waitconds :: "'n vctx \<Rightarrow> 'm vctx \<Rightarrow> ('n,'m) wconds \<Rightarrow> bool"
where
  "wt_waitconds loc sh wcs = (\<forall> wc \<in> set wcs . wt_waitcond loc sh wc)"

--"check if a stmt is well-typed"
fun wt_stmt :: "'n vctx \<Rightarrow> 'm vctx \<Rightarrow> ('pn,'n,'m,'l) stmt \<Rightarrow> bool"
where
  "wt_stmt loc sh (Cnone _)        = True"

 |"wt_stmt loc sh (Cseq _ s1 s2)   = ( wt_stmt loc sh s1 \<and> wt_stmt loc sh s2 )"

 |"wt_stmt loc sh (Casg _ x e)     = ( wt_var loc x \<and> wt_expr loc e 
                                   \<and> var_tp loc x = expr_tp loc e )"

 |"wt_stmt loc sh (Cif _ be s1 s2) = ( wt_bexpr loc be 
                                   \<and> wt_stmt loc sh s1 
                                   \<and> wt_stmt loc sh s2 )"

 |"wt_stmt loc sh (Cwhile _ be s)  = ( wt_bexpr loc be \<and> wt_stmt loc sh s )"

 |"wt_stmt loc sh (Cread _ u v)    = ( wt_var loc u \<and> wt_var sh v 
                                   \<and> var_tp loc u = var_tp sh v )"

 |"wt_stmt loc sh (Cwrite _ u e)   = ( wt_var sh u \<and> wt_expr loc e 
                                   \<and> var_tp sh u = expr_tp loc e )"

 |"wt_stmt loc sh (Cwait _ wcs s)  = (wt_waitconds loc sh wcs \<and> wt_stmt loc sh s)"

fun wt_proc :: "('pn,'n,'m,'l) proc \<Rightarrow> bool"  --"check if a process is well-typed"
where
  "wt_proc (Proc hdr s) = (wt_stmt (hdr_ctx hdr) (hdr_ctxsh hdr) s)"

fun wf_prochdr :: "('pn,'n,'m,'l) proc \<Rightarrow> bool"
where
  "wf_prochdr (Proc hdr s) = (  distinct (map vd_name (hdr_ctx hdr)) 
                              \<and> distinct (map vd_name (hdr_ctxsh hdr)) )"

fun is_sub_ctx :: "'m vctx \<Rightarrow> 'm vctx \<Rightarrow> bool"
where
  "is_sub_ctx ctx1 ctx2 = (\<forall> vd \<in> set ctx1 . 
                               var_tp ctx2 (vd_name vd) = None 
                             \<or> var_tp ctx2 (vd_name vd) = Some (vd_type vd) )"

--"check if 2 var decl lists are coherent"
fun is_coh_ctx :: "'m vctx \<Rightarrow> 'm vctx \<Rightarrow> bool"
where
  "is_coh_ctx ctx1 ctx2 = (is_sub_ctx ctx1 ctx2 \<and> is_sub_ctx ctx2 ctx1)"

--"check if a program is well-formed"
definition wf_prog :: "('pn,'n,'m,'l) prog \<Rightarrow> bool"
where
  "wf_prog prog = (  distinct (map proc_name prog) 
                   \<and> (\<forall> proc \<in> set prog . wf_prochdr proc \<and> wt_proc proc) 
                   \<and> (\<forall> proc1 \<in> set prog . \<forall> proc2 \<in> set prog . 
                           is_coh_ctx (proc_ctxsh proc1) (proc_ctxsh proc2)))"

end
